\begin{tabbing}
sendMinimalR\=\{\$a:ut2, \$tg:ut2\}\+
\\[0ex]($T$; $t$; $l$; ${\it ds}_{1}$; ${\it ds}_{2}$; $P$; $Q$; $d_{1}$; $d_{2}$; $f$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\oplus$([\=weakSendDoApplyR\=\{\$a:ut2, \$tg:ut2\}\+\+
\\[0ex]($T$; $t$; $l$; ${\it ds}_{1}$; $f$ o' mu'(State(${\it ds}_{1}$);$\lambda$$s$,$n$. $\neg_{b}$($P$($s$,$n$));$d_{1}$)) / 
\-\\[0ex][\=weakSendDoApplyR\=\{\$a:ut2, \$tg:ut2\}\+\+
\\[0ex]($\mathbb{N}$; 0; lnk{-}inv($l$); ${\it ds}_{2}$; mu'(State(${\it ds}_{2}$);$\lambda$$s$,$n$. $\neg_{b}$($Q$($s$,$n$));$d_{2}$)) / 
\-\\[0ex][]]])
\-\-
\end{tabbing}